Nuprl Lemma : zip_unzip
4,23
postcript
pdf
T1
,
T2
:Type,
as
:(
T1
T2
) List. zip(1of(unzip(
as
));2of(unzip(
as
))) =
as
latex
Definitions
unzip(
as
)
,
t
T
,
x
:
A
.
B
(
x
)
origin
T1, T2:Type, as:(T1
T2) List. zip(1of(unzip(as));2of(unzip(as))) = as T1, T2:Type, as:(T1T2) List. zip(1of(unzip(as));2of(unzip(as))) = as 
Tx:A. B(x)